1. Technical Field
The present invention relates to computer program testing and more particularly to system and methods for dynamically inferring preconditions for generating tests
2. Description of the Related Art
Data preconditions are used to specify a safe calling environment for an imperative procedure that permits its error free execution. The preconditions are used widely in software engineering practice to support, modularity by formally documenting interfaces. Such preconditions enable reliable integration testing by detecting failures closer to their sources. The preconditions also enable modular verification of large software systems.
We investigate a predicate-based approach to inferring data preconditions for low-level software libraries. The present techniques infer preconditions based on a set of predicates P={π1 . . . πm} involving the inputs to the procedure. Such predicates may be provided by the user, or extracted automatically from the procedure description.
Given a procedure and a set of predicates, predicate complete enumeration is performed to explore all the theory feasible truth assignments to the predicates. For each feasible truth combination, we derive a corresponding test case(s) to the procedures that satisfy each predicate or its negation depending on the truth assignment. The resulting executions of the test case are classified as erroneous, if at least one execution leads to a failure, or is error free, if all executions succeed. After enumerating all the feasible truth combinations of the input predicates, we obtain a truth table that classifies the truth assignments to the predicates as erroneous or error-free. Such a table represents a Boolean function over the truth assignments that predict the occurrence of an error. Expressing this Boolean function as a formula involving the predicates {π1 . . . πm} yields the needed truth combination.
If the number of predicates is large, however, a complete enumeration of all the truth value combinations is not feasible. Therefore, a statistical sampling technique is provided by combining randomized and deterministic SAT solvers with a theory satisfiable checker. A sampling technique produces a near-uniform sampling of the feasible truth values. By executing the test cases obtained from the feasible truth combinations, it is possible to classify the sampled truth combinations as erroneous or otherwise, resulting in a partial truth table. We then use a decision tree learning technique to learn a Boolean function that predicts error-free execution.
A system and method for inferring preconditions for procedures in a program includes formulating predicates based on inputs to a procedure, including formal arguments, global variables and external environment. Truth assignments are sampled to the predicates to provide truth assignments that lead to a feasible set of input values. Test cases are generated for testing the program in accordance with the truth assignments having feasible sets of input values. The truth assignments are classified to the predicates as providing an error or not providing an error.
A system implemented on computer readable medium comprising a computer readable program for inferring preconditions for procedures in a program includes a program instrumenter configured to instrument a program with variables to track properties of the program to formulate predicates which are derived from the variables and based on inputs to a procedure, including formal arguments, global variables and external environment. A satisfiability solver and theory solver are employed in combination to randomly sample truth assignments to the predicates to provide truth assignments that lead to a feasible set of input values. A test case generator is configured to test the program in accordance with the truth assignments having the feasible sets of input values and to classify the truth assignments to the predicates as providing an error or not providing an error. A decision tree learning method is configured to infer preconditions on the inputs to the procedure based upon classified truth assignments.
These and other features and advantages will become apparent from the following detailed description of illustrative embodiments thereof, which is to be read in connection with the accompanying drawings.